lexer grammar TBTLexer;

/* Virtual token for tokens for representing indentation */
tokens{
  SPATIU;
  INDENT;
  DEDENT;
}

@lexer::members{
  int open = 0;
}

@header {
  package parser;
}


FORALL  : '\\/';
ARROW   : '->';
TLAMBDA : '/\\';
LAMBDA  : 'fn';
DOT     : '.';
SEMI    : ':';
EQ      : '=';
BIND    : ':=';
OR      : '|';
DARROW  : '=>';
STAR    : '*';

LETREC  : 'letrec';
LET     : 'let';
CASE    : 'case';
OF      : 'of';
IND     : 'Inductive';
COIND   : 'Coinductive';

LPAREN  : '(';
RPAREN  : ')';

LCURLY  : '{';
RCURLY  : '}';

LANG    : '<';
RANG    : '>'; 

COLUMN  : ';';

ID  : ('a'..'z'|'0'..'9')('a'..'z'|'A'..'Z'|'0'..'9'|'_')* | '\\'.
    ;

TID : ('A'..'Z') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')*
    ; 

// TODO: Layout indentation
    
WS  :   (' '|'\t' |'\n'|'\r')+  { skip();}
    ;

COMMENT
    :   '#' ~('\n'|'\r')*    {skip();}
    |   '---' ~('\n'|'\r')*  {skip();}
    |   '//' ~('\n'|'\r')*   {skip();}
    |   '(*' (options {greedy=false;} : .)* '*)'  {skip();}
    ;

